(declare-sort U)

(declare-fun a_464 () (Array Int Int))
(declare-fun i_465 () Int)
(declare-fun a_460 () (Array Int Int))
(assert (and (= 0 (select a_460 0)) (not (= a_460 (store a_464 i_465 1)))))
(check-sat)
(declare-fun f (Int) U)
(declare-fun g (Int) U)
(declare-fun h (U) Int)
(assert (< 1 (h (g 1))))
(assert (= (g 0) (f 0)))
(declare-fun Q (U Int) Bool)
(declare-const c U)
(assert (forall ((x U) (y Int)) (or (Q x y) (and (not (= x c)) (not (= x (f y)))))))
(check-sat)
(declare-const __ (_ BitVec 1))
(declare-const x4 Bool)
(declare-fun f ((_ BitVec 8)) (_ BitVec 8))
(assert (and (distinct (_ bv0 8) (f (_ bv0 8))) (forall ((x (_ BitVec 8))) (or x4 (distinct (f x) (f (_ bv0 8)))))))
(assert (= (_ bv0 8) (f (concat (_ bv1 7) ((_ extract 0 0) __)))))
(check-sat)
